COMMENT ⊗   VALID 00009 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	the notions of finite union and finite sum
C00006 00003	(proof sumfacts)
C00008 00004	miscellaneous facts
C00010 00005	* bound quantifier
C00015 00006	proof of properties of union and sum
C00017 00007	proofs 
C00021 00008	proof of properties of mkset,mklset                   ***try again***
C00024 00009	mklset_un                                             ***try again***
C00027 ENDMK
C⊗;
;the notions of finite union and finite sum
(wipe-out)
(get-proofs appl)
(proof sums)

(decl all (type: |ground⊗@set→truthval|) (syntype: constant))
(decl some (type: |ground⊗@set→truthval|) (syntype: constant))
(decl (numseq f) (type:|ground→ground|))
(decl sum (type: |(@numseq)⊗(@n)→(@n)|) (syntype: constant))
(decl setseq (type: |@n→@set|))
(decl un (type: |(@setseq)⊗(@n)→(@set)|) (syntype: constant))

;axiom for all
(defax all |∀n a.all(0,a)∧(all(n',a)≡a(n)∧all(n,a))|)
(label alldef)

;axiom for some
(defax some |∀n a.¬some(0,a)∧(some(n',a)≡a(n)∨some(n,a))|)
(label somedef)

;axiom for sum
(defax sum |∀n numseq.sum(numseq,0)=0∧sum(numseq,n')=sum(numseq,n)+numseq(n)|)
(label sumdef)

;axiom for un
(defax un |∀n setseq.un(setseq,0)=emptyset∧un(setseq,n')=un(setseq,n)∪setseq(n)|)
(label undef)

(decl disj_pair (type: |(@set⊗@set)→truthval|))
(define disj_pair |∀a b.disj_pair(a,b)=emptyp(a∩b)|)
(label dijpair_def)

(decl disjoint (type: |((ground→@set)⊗ground)→truthval|))
(defax disjoint |∀n setseq.disjoint(setseq,0)∧
    disjoint(setseq,n')=(disjoint(setseq,n)∧disj_pair(un(setseq,n),setseq(n)))| )
(label disjointdef)
(proof sumfacts)

;properties of all and some

(axiom |∀a n.(∀m.m<n⊃a(m))≡all(n,a)|)
(label allfact)

(axiom |∀a n.(∃m.m<n∧a(m))≡some(n,a)|)
(label somefact)

;properties of un

(axiom |∀setseq n m.m<n⊃setseq(m)⊂un(setseq,n)|)
(label unionfact1)

;exercise: unionfact2 
;∀setseq n m.n<m⊃un(setseq,n)⊂un(setseq,m)

;properties of sum

(axiom |∀k numseq.natnum(numseq(k))|) 
(label simpinfo)(label numseq_total)

(axiom |∀k numseq.natnum(sum(numseq,k))|)
(label simpinfo)(label sumsort)

;miscellaneous facts
;facts about mkset, mklset and union

(proof unionfacts)

(axiom |∀u n.n≤length u⊃(un(λm.mkset(nth(u,m)),n))=(λx.(∃k.k<n∧nth(u,k)=x))|)
(label mksetfact)

(axiom |∀u.un(λm.mkset(nth(u,m)),length u)=(λx.(mklset(u))(x))|)
(label mklset_un)

(save-proofs sums)
;* bound quantifier
    (proof allprop)

    ;we can easily prove that `all' does its job

1.  (ue ((a.|λn.all(n,a)⊃(m<n⊃a(m))|)) proof_by_induction
	 ((use transitivity_of_order) (use successor1) (open all)
	   (use less_succ_lesseq normal mode: exact) (open lesseq)))
    ;∀N.ALL(N,A)⊃(M<N⊃A(M))

2.  (ue ((a.|λn.(∀m.m<n⊃a(m))⊃all(n,a)|)) proof_by_induction (open all)
	  (use normal mode: always)
	  (use less_succ_lesseq mode: exact) (open lesseq)))
    ;∀N.(∀M.M<N⊃A(M))⊃ALL(N,A)

3.  (derive |∀n.(∀m.m<n⊃a(m))≡all(n,a)| (* -2))

    ;similarly for `some':

4.  (ue ((a.|λn.some(n,a)⊃(∃m.m<n∧a(m))|)) proof_by_induction
	 ((use transitivity_of_order) (use successor1) (open some) (part 1 (der))
	   (use less_succ_lesseq normal mode: exact) (open lesseq)))
    ;∀N.SOME(N,A)⊃(∃M.M<N∧A(M))

5.  (ue ((a.|λn.(∃m.m<n∧a(m))⊃some(n,a)|)) proof_by_induction (open some)
	  (use normal mode: always) (part 1(der))
	  (use less_succ_lesseq mode: exact) (open lesseq)))
    ;∀N.(∃M.M<N∧A(M))⊃SOME(N,A)

6.  (derive |∀n.(∃m.m<n∧a(m))≡some(n,a)| (* -2))

;proof of properties of union and sum
(wipe-out)
(get-proofs sums)
(proof unionfacts)

;a property of union

;unionfact1

(ue (a |λn.m<n⊃(∀xv.(setseq(m))(xv)⊃(un(setseq,n))(xv))|) proof_by_induction
   (open un union) 
    (use less_succ_lesseq mode: always) (open lesseq) (use normal mode: always))
;∀N.M<N⊃(∀XV.(SETSEQ(M))(XV)⊃(UN(SETSEQ,N))(XV))

;a property of sum

;sumsort

(unlabel simpinfo sumsort)
(ue (a |λn.natnum(sum(numseq,n))|) proof_by_induction (open sum))
;∀N.NATNUM(SUM(NUMSEQ,N))
(label simpinfo sumsort)

;proofs 
(wipe-out)
(get-proofs sums)

(proof normal)
(derive |∀p q r.(p≡q)⊃(p∨r≡r∨q)|)
(label equiv_disj)


(proof unionprop)

(ue (a |λn.n≤length u⊃
                (un(λm.mkset(nth(u,m)),n))(x)≡some(n,λk.x=nth(u,k))|)
    proof_by_induction 
    (part 1(open un mkset nth some union emptyset) equiv_disj (der))
    (use succ_lesseq_lesseq mode: always))
;∀N.N≤LENGTH U⊃(UN(λM.MKSET(NTH(U,M)),N))(X)≡SOME(N,λK.X=NTH(U,K))

(rw -2 (use somefact 
        ue: ((a.|λk.x=nth(u,k)|)(n.n)) mode: exact direction: reverse))
;∀N.N≤LENGTH U⊃(UN(λM.MKSET(NTH(U,M)),N))(X)≡(∃M.M<N∧X=NTH(U,M))

(assume |n≤length u|)

(ue ((av.|un(λm.mkset nth(u,m),n)|)
     (bv.|λx.∃k.k<n∧nth(u,k)=x|)) set_extensionality 
     (open epsilon)(use * -2 mode: always))
;UN(λM.MKSET(NTH(U,M)),N)=(λX.(∃K.K<N∧NTH(U,K)=X))

(ci -2)
;N≤LENGTH U⊃UN(λM.MKSET(NTH(U,M)),N)=(λX.(∃K.K<N∧NTH(U,K)=X))

;;;;;;;
;labels: TRANS_LESSEQ 
;∀N M K.N≤M∧M≤K⊃N≤K

;labels: SET_EXTENSIONALITY 
;∀AV BV.(∀XV.XVεAV≡XVεBV)⊃AV=BV

;labels: SOMEFACT 
;∀A N.(∃M.M<N∧A(M))≡SOME(N,A)

;proof of properties of mkset,mklset                   ***try again***
(wipe-out)
(get-proofs nth)

(proof mkset)
 
(assume |n≤length u∧(un(λm.mkset nth(u,m),n))(xv)⊃(∃k.k<n∧nth(u,k)=xv)|)
(label mks1)

(assume |n'≤length u|)
(label mks2)

(assume |(un(λm.mkset nth(u,m),n'))(xv)|)
(label mks3)

(rw * (open un union emptyset))
;(UN(λM.MKSET(NTH(U,M)),N))(XV)∨(MKSET(NTH(U,N)))(XV)
(label mks4)

(assume |(un(λm.mkset nth(u,m),n))(xv)|)
(label mks5)

(derive |∃k.k<n∧nth(u,k)=xv|(mks1 * mks2 succ_lesseq_lesseq))

(derive |∃k.k<n'∧nth(u,k)=xv|(* transitivity_of_order successor1))
(label mks6)

(assume |(mkset nth(u,n))(xv)|)
(label mks7)

(rw * (open mkset))
;XV=NTH(U,N)
(derive |∃k.k<n'∧nth(u,k)=xv| (* successor1))

(cases mks4 mks6 *)
;∃K.K<N'∧NTH(U,K)=XV
;deps: (MKS1 MKS2 MKS3)

(ci (mks2 mks3))
;N'≤LENGTH U∧(UN(λM.MKSET(NTH(U,M)),N'))(XV)⊃(∃K.K<N'∧NTH(U,K)=XV)

(ci mks1)

(ue (a |λn.n≤length u∧(un(λm.mkset nth(u,m),n))(xv)⊃(∃k.k<n∧nth(u,k)=xv)|)
   proof_by_induction (part 1#1(open un emptyset)) *)
;∀N.N≤LENGTH U∧(UN(λM.MKSET(NTH(U,M)),N))(XV)⊃(∃K.K<N∧NTH(U,K)=XV)
(label mks8)

;the other direction is trivial

(assume |∃k.k<n∧nth(u,k)=xv|)
(label mks11)

(define kv |kv<n∧nth(u,kv)=xv| *)
(label mks12)

(ue ((setseq.|λk.mkset nth(u,k)|)(m.|kv|)(n.|n|)) unionfact1 (open inclusion))
;KV<N⊃(∀XV.(MKSET(NTH(U,KV)))(XV)⊃(UN(λK.MKSET(NTH(U,K)),N))(XV))
(label mks13)

(trw |(mkset nth(u,kv))(xv)| (open mkset) mks12)
;(MKSET(NTH(U,KV)))(XV)

(derive |(un(λk.mkset(nth(u,k)),n))(xv)|(mks13 mks12 *))
;deps: (MKS12)

(ci mks11)
;(∃K.K<N∧NTH(U,K)=XV)⊃(UN(λK.MKSET(NTH(U,K)),N))(XV)

(derive |∀n.n≤length u∧(un(λm.mkset nth(u,m),n))(xv)≡(∃k.k<n∧nth(u,k)=xv)|(mks8 *))
;mklset_un                                             ***try again***

(ue (n |length u|) mksetfact 
    (use mklset_fact mode: exact direction: reverse) (open lesseq))
;∀U.UN(λM.MKSET(NTH(U,M)),LENGTH U)=(λX.(MKLSET(U))(XV))